Inference at * 
Iof proof for Lemma complete nat ind:


  P:({k}). (i:. (j:i. P(j))  P(i))  (i:. P(i)) 

latex

 by (Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t) inil_term) 

latex

 1: 

 1: 1. P : {k}
 1: 2. i:. (j:i. P(j))  P(i)
 1: 3. i : 
 1:   P(i)
 .

Definitions	t  T, x(s), P  Q, , , x:A. B(x), P  Q, i  j < k, {i..j}
Lemmas	le wf, int seg wf, nat wf